\begin{tabbing}
es{-}sends{-}iff(${\it es}$;$l$;${\it tgs}$;${\it da}$;${\it ds}$;$e$.$f$($e$))
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(\=$\forall$$e$:es{-}E(${\it es}$).\+\+
\\[0ex]es{-}isrcv(${\it es}$; $e$)
\\[0ex]$\Rightarrow$ es{-}lnk(${\it es}$; $e$) $=$ $l$ $\in$ IdLnk
\\[0ex]$\Rightarrow$ (\=$\exists$${\it e'}$:es{-}E(${\it es}$).\+
\\[0ex]es{-}isrcv(${\it es}$; ${\it e'}$)
\\[0ex]\& \=es{-}lnk(${\it es}$; ${\it e'}$) $=$ $l$ $\in$ IdLnk\+
\\[0ex]\& (es{-}tag(${\it es}$; ${\it e'}$) $\in$ ${\it tgs}$ $\in$ Id)
\\[0ex]\& es{-}sender(${\it es}$; ${\it e'}$) $=$ es{-}sender(${\it es}$; $e$) $\in$ es{-}E(${\it es}$))
\-\-\\[0ex]$\Rightarrow$ (es{-}tag(${\it es}$; $e$) $\in$ ${\it tgs}$ $\in$ Id))
\-\\[0ex]\& (\=$\forall$${\it e'}$:es{-}E(${\it es}$).\+
\\[0ex]es{-}isrcv(${\it es}$; ${\it e'}$)
\\[0ex]$\Rightarrow$ es{-}lnk(${\it es}$; ${\it e'}$) $=$ $l$ $\in$ IdLnk
\\[0ex]$\Rightarrow$ (es{-}tag(${\it es}$; ${\it e'}$) $\in$ ${\it tgs}$ $\in$ Id)
\\[0ex]$\Rightarrow$ es{-}valtype(${\it es}$; ${\it e'}$) $\subseteq\rho$ fpf{-}cap(${\it da}$;KindDeq;es{-}kind(${\it es}$; ${\it e'}$);Void))
\-\\[0ex]\& ($\forall$$x$:Id. es{-}vartype(${\it es}$; source($l$); $x$) $\subseteq\rho$ fpf{-}cap(${\it ds}$;IdDeq;$x$;Top))
\\[0ex]\& \=alle{-}at(${\it es}$;source($l$);$e$.$\forall$$i$:\{0..$\parallel$$f$($e$)$\parallel^{-}$\}.\+
\\[0ex]$\exists$${\it e'}$:es{-}E(${\it es}$).
\\[0ex]es{-}isrcv(${\it es}$; ${\it e'}$)
\\[0ex]\& es{-}lnk(${\it es}$; ${\it e'}$) $=$ $l$ $\in$ IdLnk
\\[0ex]\& (es{-}tag(${\it es}$; ${\it e'}$) $\in$ ${\it tgs}$ $\in$ Id)
\\[0ex]\& es{-}sender(${\it es}$; ${\it e'}$) $=$ $e$ $\in$ es{-}E(${\it es}$)
\\[0ex]\& es{-}index(${\it es}$; ${\it e'}$) $=$ $i$ $\in$ $\mathbb{Z}$)
\\[0ex]\& (\=$\forall$${\it e'}$:es{-}E(${\it es}$).\+
\\[0ex]es{-}isrcv(${\it es}$; ${\it e'}$)
\\[0ex]$\Rightarrow$ es{-}lnk(${\it es}$; ${\it e'}$) $=$ $l$ $\in$ IdLnk
\\[0ex]$\Rightarrow$ (es{-}tag(${\it es}$; ${\it e'}$) $\in$ ${\it tgs}$ $\in$ Id)
\\[0ex]$\Rightarrow$ \=es{-}index(${\it es}$; ${\it e'}$)$<\parallel$$f$(es{-}sender(${\it es}$; ${\it e'}$))$\parallel$\+
\\[0ex]\& \=$\langle$es{-}tag(${\it es}$; ${\it e'}$)$,\,$es{-}val(${\it es}$; ${\it e'}$)$\rangle$\+
\\[0ex]$=$
\\[0ex]$f$(es{-}sender(${\it es}$; ${\it e'}$))[es{-}index(${\it es}$; ${\it e'}$)]
\\[0ex]$\in$ ${\it tg}$:Id$\times$fpf{-}cap(${\it da}$;KindDeq;rcv($l$,${\it tg}$);Void))
\-\-\-\-\-
\end{tabbing}